mcsta

Benchmark
Model:pnueli-zuck v.1 (MDP)
Parameter(s)N = 10
Property:live (prob-reach)
Invocation (specific)
mcsta/modest mcsta pnueli-zuck.10.jani --props live -O out.txt Minimal --unsafe --es -S Hybrid --store-compress None --no-partial-results --p0 --p1 --epsilon 0 --absolute-epsilon
Execution
Walltime:> 1800s (Timeout)
Log
pnueli-zuck.10.jani:model: info: pnueli-zuck.10 is an MDP model.
pnueli-zuck.10.jani:variables[0]: info: Expanding variable "p0" into 16 locations in automaton "process0".
pnueli-zuck.10.jani:variables[1]: info: Expanding variable "p1" into 16 locations in automaton "process1".
pnueli-zuck.10.jani:variables[2]: info: Expanding variable "p2" into 16 locations in automaton "process2".
pnueli-zuck.10.jani:variables[3]: info: Expanding variable "p3" into 16 locations in automaton "process3".
pnueli-zuck.10.jani:variables[4]: info: Expanding variable "p4" into 16 locations in automaton "process4".
pnueli-zuck.10.jani:variables[5]: info: Expanding variable "p5" into 16 locations in automaton "process5".
pnueli-zuck.10.jani:variables[6]: info: Expanding variable "p6" into 16 locations in automaton "process6".
pnueli-zuck.10.jani:variables[7]: info: Expanding variable "p7" into 16 locations in automaton "process7".
pnueli-zuck.10.jani:variables[8]: info: Expanding variable "p8" into 16 locations in automaton "process8".
pnueli-zuck.10.jani:variables[9]: info: Expanding variable "p9" into 16 locations in automaton "process9".
pnueli-zuck.10.jani: info: Need 24 bytes per state.
STDERR
The Modest Toolset (www.modestchecker.net), version v3.1.42-gb5e9d523c.


----------
Computation aborted after 1800.4651749134064 seconds since the total time limit of 1800 seconds was exceeded.